es:ES, C, T:Type, R1, R2:(CE), decodes1:(i:Ce:{x:E| R1(i,x)} state@loc(e)T),
decodes2:(i:Ce:{x:E| R2(i,x)} state@loc(e)T), dec_R1:(i:Ce:EDec(R1(i,e))).
(i:C, e:E. (R1(i,e) & R2(i,e)))
 (i:C, e:{x:E| (R1(i,x))  (R2(i,x))} , st:state@loc(e).
 ((R1(i,e))  ([R1 ? decodes1 : decodes2](i,e,st) = decodes1(i,e,st)))
 & ((R2(i,e))  ([R1 ? decodes1 : decodes2](i,e,st) = decodes2(i,e,st)))) 

latex

Definitions	P  Q, s = t, <a, b>, [R ? decodes1 : decodes2], P  Q, left + right, A, P & Q, x:A  B(x), Dec(P), {x:A| B(x)} , f(a), state@i, loc(e), x:AB(x), E, x:A. B(x), , Type, t  T, ES, if p:P then A(p) else B fi , False
Lemmas	event system wf, es-E wf, es-loc wf, es-state wf, decidable wf, not wf